Sau đây là định nghĩa và ý nghĩa của các quy tắc cơ bản (trong đó, P và Q là 2 thực thể cần liên lạc với nhau, X là một văn bản/gói tin còn K là khóa)

• P believes X: P coi X là đúng và có thể xác nhận X trong các gói tin khác.
• P has jurisdiction over X: Sự tin tưởng của P đối với X là có cơ sở.
• P said X: Tại một thời điểm trong quá khứ, P đã gửi (và tin) X, mặc dầu hiện tại P có thể không còn tin vào X.
• P sees X: P đã nhận được X, có thể đọc và gửi lại X.
• {X}K: X được mật mã hóa với khóa K.
• fresh(X): X vừa mới được tạo ra và gửi đi.
• key(K, P<->Q): P và Q có chung khóa K để trao đổi thông tin mật.

Ý nghĩa của các định nghĩa trên có thể được diễn giải thông qua một số định đề sau:

• Nếu P believes key(K, P<->Q), và P sees {X}K, thì P believes (Q said X)
• Nếu P believes (Q said X) và P believes fresh(X), thì P believes (Q believes X).

Ở đây, P phải tin tưởng rằng gói tin X là mới được tạo ra (fresh). Ngược lại, X có thể là một gói tin cũ được một kẻ tấn công nào đó thu và phát lại.

• Nếu P believes (Q has jurisdiction over X) và P believes (Q believes X), thì P believes X
• Có một số phương pháp để xử lý việc kết hợp (ghép) các gói tin. Chẳng hạn, nếu P believes that Q said <X, Y>, bản tin ghép X và Y, thì P cũng cho rằng Q said X và Q said Y.

Với phương pháp biểu diễn nêu trên, các giả định đằng sau các giao thức xác thực có thể được chuẩn hóa. Sử dụng các định đề, ta có thể chứng minh một thực thể nào đó tin tưởng rằng họ có thể thực hiện giao dịch an toàn với một vài khóa nhất định. Nếu chứng minh cho kết quả ngược lại (không đảm bảo an toàn), thì kết quả thường chỉ ra cách thức mà kẻ tấn công có thể thực hiện.